\begin{tabbing} $\forall$\=${\it poss}$:(ES\{i\}$\rightarrow\mathbb{P}$\{i'\}), $R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow\mathbb{P}$\{i'\}), $P$,\+ \\[0ex]$Q$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow\mathbb{P}$\{i'\}). \-\\[0ex]($\forall$$e$:possible{-}event\{i:l\}(${\it poss}$). ($P$($e$)) $\Rightarrow$ ($Q$($e$))) \\[0ex]$\Rightarrow$ \=($\forall$$e$:possible{-}event\=\{i:l\}\+\+ \\[0ex](${\it poss}$). \-\\[0ex]es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e$) $\Rightarrow$ es{-}knows\{i:l\}(${\it poss}$; $R$; $Q$; $e$)) \- \end{tabbing}